0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CpxRNTS
↳13 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CpxRNTS
↳15 IntTrsBoundProof (UPPER BOUND(ID), 464 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 180 ms)
↳18 CpxRNTS
↳19 FinalProof (⇔, 0 ms)
↳20 BOUNDS(1, n^1)
eq0(S(x'), S(x)) → eq0(x', x)
eq0(S(x), 0) → 0
eq0(0, S(x)) → 0
eq0(0, 0) → S(0)
eq0(S(x'), S(x)) → eq0(x', x) [1]
eq0(S(x), 0) → 0 [1]
eq0(0, S(x)) → 0 [1]
eq0(0, 0) → S(0) [1]
eq0(S(x'), S(x)) → eq0(x', x) [1]
eq0(S(x), 0) → 0 [1]
eq0(0, S(x)) → 0 [1]
eq0(0, 0) → S(0) [1]
eq0 :: S:0 → S:0 → S:0 S :: S:0 → S:0 0 :: S:0 |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
eq0
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
eq0(z, z') -{ 1 }→ eq0(x', x) :|: z = 1 + x', z' = 1 + x, x' >= 0, x >= 0
eq0(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
eq0(z, z') -{ 1 }→ 0 :|: z' = 1 + x, x >= 0, z = 0
eq0(z, z') -{ 1 }→ 1 + 0 :|: z = 0, z' = 0
eq0(z, z') -{ 1 }→ eq0(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eq0(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
eq0(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq0(z, z') -{ 1 }→ 1 + 0 :|: z = 0, z' = 0
{ eq0 } |
eq0(z, z') -{ 1 }→ eq0(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eq0(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
eq0(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq0(z, z') -{ 1 }→ 1 + 0 :|: z = 0, z' = 0
eq0(z, z') -{ 1 }→ eq0(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eq0(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
eq0(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq0(z, z') -{ 1 }→ 1 + 0 :|: z = 0, z' = 0
eq0: runtime: ?, size: O(1) [1] |
eq0(z, z') -{ 1 }→ eq0(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eq0(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
eq0(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq0(z, z') -{ 1 }→ 1 + 0 :|: z = 0, z' = 0
eq0: runtime: O(n1) [1 + z'], size: O(1) [1] |